Report for Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/merge_sort_true-unreach-call/merge_sort_true-unreach-call.c (Counterexample 13)

Generated on 2025-08-28 07:02:22 by CPAchecker 4.0 / terminationAnalysis

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

Rank
Scope
-V-
{{line.bestrank}}
{{line.desc}}
Precondition (initial variable assignment):

{{precondition}}

{{fault.rank}}. {{fault.score}} Details:
Current values:
Name Value
1
extern void __VERIFIER_error() __attribute__ ((__noreturn__));  
2
  
3
typedef long unsigned int size_t;  
4
typedef int wchar_t;  
5
  
6
union wait  
7
  {  
8
    int w_status;  
9
    struct  
10
      {  
11
 unsigned int __w_termsig:7;  
12
 unsigned int __w_coredump:1;  
13
 unsigned int __w_retcode:8;  
14
 unsigned int:16;  
15
      } __wait_terminated;  
16
    struct  
17
      {  
18
 unsigned int __w_stopval:8;  
19
 unsigned int __w_stopsig:8;  
20
 unsigned int:16;  
21
      } __wait_stopped;  
22
  };  
23
typedef union  
24
  {  
25
    union wait *__uptr;  
26
    int *__iptr;  
27
  } __WAIT_STATUS __attribute__ ((__transparent_union__));  
28
  
29
typedef struct  
30
  {  
31
    int quot;  
32
    int rem;  
33
  } div_t;  
34
typedef struct  
35
  {  
36
    long int quot;  
37
    long int rem;  
38
  } ldiv_t;  
39
  
40
  
41
__extension__ typedef struct  
42
  {  
43
    long long int quot;  
44
    long long int rem;  
45
  } lldiv_t;  
46
  
47
extern size_t __ctype_get_mb_cur_max (void) __attribute__ ((__nothrow__ , __leaf__)) ;  
48
  
49
extern double atof (__const char *__nptr)  
50
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;  
51
extern int atoi (__const char *__nptr)  
52
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;  
53
extern long int atol (__const char *__nptr)  
54
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;  
55
  
56
  
57
__extension__ extern long long int atoll (__const char *__nptr)  
58
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;  
59
  
60
  
61
extern double strtod (__const char *__restrict __nptr,  
62
        char **__restrict __endptr)  
63
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
64
  
65
  
66
extern float strtof (__const char *__restrict __nptr,  
67
       char **__restrict __endptr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
68
extern long double strtold (__const char *__restrict __nptr,  
69
       char **__restrict __endptr)  
70
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
71
  
72
  
73
extern long int strtol (__const char *__restrict __nptr,  
74
   char **__restrict __endptr, int __base)  
75
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
76
extern unsigned long int strtoul (__const char *__restrict __nptr,  
77
      char **__restrict __endptr, int __base)  
78
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
79
  
80
__extension__  
81
extern long long int strtoq (__const char *__restrict __nptr,  
82
        char **__restrict __endptr, int __base)  
83
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
84
__extension__  
85
extern unsigned long long int strtouq (__const char *__restrict __nptr,  
86
           char **__restrict __endptr, int __base)  
87
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
88
  
89
__extension__  
90
extern long long int strtoll (__const char *__restrict __nptr,  
91
         char **__restrict __endptr, int __base)  
92
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
93
__extension__  
94
extern unsigned long long int strtoull (__const char *__restrict __nptr,  
95
     char **__restrict __endptr, int __base)  
96
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
97
  
98
extern char *l64a (long int __n) __attribute__ ((__nothrow__ , __leaf__)) ;  
99
extern long int a64l (__const char *__s)  
100
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;  
101
  
102
typedef unsigned char __u_char;  
103
typedef unsigned short int __u_short;  
104
typedef unsigned int __u_int;  
105
typedef unsigned long int __u_long;  
106
typedef signed char __int8_t;  
107
typedef unsigned char __uint8_t;  
108
typedef signed short int __int16_t;  
109
typedef unsigned short int __uint16_t;  
110
typedef signed int __int32_t;  
111
typedef unsigned int __uint32_t;  
112
typedef signed long int __int64_t;  
113
typedef unsigned long int __uint64_t;  
114
typedef long int __quad_t;  
115
typedef unsigned long int __u_quad_t;  
116
typedef unsigned long int __dev_t;  
117
typedef unsigned int __uid_t;  
118
typedef unsigned int __gid_t;  
119
typedef unsigned long int __ino_t;  
120
typedef unsigned long int __ino64_t;  
121
typedef unsigned int __mode_t;  
122
typedef unsigned long int __nlink_t;  
123
typedef long int __off_t;  
124
typedef long int __off64_t;  
125
typedef int __pid_t;  
126
typedef struct { int __val[2]; } __fsid_t;  
127
typedef long int __clock_t;  
128
typedef unsigned long int __rlim_t;  
129
typedef unsigned long int __rlim64_t;  
130
typedef unsigned int __id_t;  
131
typedef long int __time_t;  
132
typedef unsigned int __useconds_t;  
133
typedef long int __suseconds_t;  
134
typedef int __daddr_t;  
135
typedef long int __swblk_t;  
136
typedef int __key_t;  
137
typedef int __clockid_t;  
138
typedef void * __timer_t;  
139
typedef long int __blksize_t;  
140
typedef long int __blkcnt_t;  
141
typedef long int __blkcnt64_t;  
142
typedef unsigned long int __fsblkcnt_t;  
143
typedef unsigned long int __fsblkcnt64_t;  
144
typedef unsigned long int __fsfilcnt_t;  
145
typedef unsigned long int __fsfilcnt64_t;  
146
typedef long int __ssize_t;  
147
typedef __off64_t __loff_t;  
148
typedef __quad_t *__qaddr_t;  
149
typedef char *__caddr_t;  
150
typedef long int __intptr_t;  
151
typedef unsigned int __socklen_t;  
152
typedef __u_char u_char;  
153
typedef __u_short u_short;  
154
typedef __u_int u_int;  
155
typedef __u_long u_long;  
156
typedef __quad_t quad_t;  
157
typedef __u_quad_t u_quad_t;  
158
typedef __fsid_t fsid_t;  
159
typedef __loff_t loff_t;  
160
typedef __ino_t ino_t;  
161
typedef __dev_t dev_t;  
162
typedef __gid_t gid_t;  
163
typedef __mode_t mode_t;  
164
typedef __nlink_t nlink_t;  
165
typedef __uid_t uid_t;  
166
typedef __off_t off_t;  
167
typedef __pid_t pid_t;  
168
typedef __id_t id_t;  
169
typedef __ssize_t ssize_t;  
170
typedef __daddr_t daddr_t;  
171
typedef __caddr_t caddr_t;  
172
typedef __key_t key_t;  
173
  
174
typedef __clock_t clock_t;  
175
  
176
  
177
  
178
typedef __time_t time_t;  
179
  
180
  
181
typedef __clockid_t clockid_t;  
182
typedef __timer_t timer_t;  
183
typedef unsigned long int ulong;  
184
typedef unsigned short int ushort;  
185
typedef unsigned int uint;  
186
typedef int int8_t __attribute__ ((__mode__ (__QI__)));  
187
typedef int int16_t __attribute__ ((__mode__ (__HI__)));  
188
typedef int int32_t __attribute__ ((__mode__ (__SI__)));  
189
typedef int int64_t __attribute__ ((__mode__ (__DI__)));  
190
typedef unsigned int u_int8_t __attribute__ ((__mode__ (__QI__)));  
191
typedef unsigned int u_int16_t __attribute__ ((__mode__ (__HI__)));  
192
typedef unsigned int u_int32_t __attribute__ ((__mode__ (__SI__)));  
193
typedef unsigned int u_int64_t __attribute__ ((__mode__ (__DI__)));  
194
typedef int register_t __attribute__ ((__mode__ (__word__)));  
195
typedef int __sig_atomic_t;  
196
typedef struct  
197
  {  
198
    unsigned long int __val[(1024 / (8 * sizeof (unsigned long int)))];  
199
  } __sigset_t;  
200
typedef __sigset_t sigset_t;  
201
struct timespec  
202
  {  
203
    __time_t tv_sec;  
204
    long int tv_nsec;  
205
  };  
206
struct timeval  
207
  {  
208
    __time_t tv_sec;  
209
    __suseconds_t tv_usec;  
210
  };  
211
typedef __suseconds_t suseconds_t;  
212
typedef long int __fd_mask;  
213
typedef struct  
214
  {  
215
    __fd_mask __fds_bits[1024 / (8 * (int) sizeof (__fd_mask))];  
216
  } fd_set;  
217
typedef __fd_mask fd_mask;  
218
  
219
extern int select (int __nfds, fd_set *__restrict __readfds,  
220
     fd_set *__restrict __writefds,  
221
     fd_set *__restrict __exceptfds,  
222
     struct timeval *__restrict __timeout);  
223
extern int pselect (int __nfds, fd_set *__restrict __readfds,  
224
      fd_set *__restrict __writefds,  
225
      fd_set *__restrict __exceptfds,  
226
      const struct timespec *__restrict __timeout,  
227
      const __sigset_t *__restrict __sigmask);  
228
  
229
  
230
__extension__  
231
extern unsigned int gnu_dev_major (unsigned long long int __dev)  
232
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));  
233
__extension__  
234
extern unsigned int gnu_dev_minor (unsigned long long int __dev)  
235
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));  
236
__extension__  
237
extern unsigned long long int gnu_dev_makedev (unsigned int __major,  
238
            unsigned int __minor)  
239
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));  
240
  
241
typedef __blksize_t blksize_t;  
242
typedef __blkcnt_t blkcnt_t;  
243
typedef __fsblkcnt_t fsblkcnt_t;  
244
  
245
  
246
typedef __fsfilcnt_t fsfilcnt_t;  
247
typedef unsigned long int pthread_t;  
248
typedef union  
249
{  
250
  char __size[56];  
251
  long int __align;  
252
} pthread_attr_t;  
253
typedef struct __pthread_internal_list  
254
{  
255
  struct __pthread_internal_list *__prev;  
256
  struct __pthread_internal_list *__next;  
257
} __pthread_list_t;  
258
typedef union  
259
{  
260
  struct __pthread_mutex_s  
261
  {  
262
    int __lock;  
263
    unsigned int __count;  
264
    int __owner;  
265
    unsigned int __nusers;  
266
    int __kind;  
267
    int __spins;  
268
    __pthread_list_t __list;  
269
  } __data;  
270
  char __size[40];  
271
  long int __align;  
272
} pthread_mutex_t;  
273
typedef union  
274
{  
275
  char __size[4];  
276
  int __align;  
277
} pthread_mutexattr_t;  
278
typedef union  
279
{  
280
  struct  
281
  {  
282
    int __lock;  
283
    unsigned int __futex;  
284
    __extension__ unsigned long long int __total_seq;  
285
    __extension__ unsigned long long int __wakeup_seq;  
286
    __extension__ unsigned long long int __woken_seq;  
287
    void *__mutex;  
288
    unsigned int __nwaiters;  
289
    unsigned int __broadcast_seq;  
290
  } __data;  
291
  char __size[48];  
292
  __extension__ long long int __align;  
293
} pthread_cond_t;  
294
typedef union  
295
{  
296
  char __size[4];  
297
  int __align;  
298
} pthread_condattr_t;  
299
typedef unsigned int pthread_key_t;  
300
typedef int pthread_once_t;  
301
typedef union  
302
{  
303
  struct  
304
  {  
305
    int __lock;  
306
    unsigned int __nr_readers;  
307
    unsigned int __readers_wakeup;  
308
    unsigned int __writer_wakeup;  
309
    unsigned int __nr_readers_queued;  
310
    unsigned int __nr_writers_queued;  
311
    int __writer;  
312
    int __shared;  
313
    unsigned long int __pad1;  
314
    unsigned long int __pad2;  
315
    unsigned int __flags;  
316
  } __data;  
317
  char __size[56];  
318
  long int __align;  
319
} pthread_rwlock_t;  
320
typedef union  
321
{  
322
  char __size[8];  
323
  long int __align;  
324
} pthread_rwlockattr_t;  
325
typedef volatile int pthread_spinlock_t;  
326
typedef union  
327
{  
328
  char __size[32];  
329
  long int __align;  
330
} pthread_barrier_t;  
331
typedef union  
332
{  
333
  char __size[4];  
334
  int __align;  
335
} pthread_barrierattr_t;  
336
  
337
extern long int random (void) __attribute__ ((__nothrow__ , __leaf__));  
338
extern void srandom (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));  
339
extern char *initstate (unsigned int __seed, char *__statebuf,  
340
   size_t __statelen) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));  
341
  
342
  
343
extern char *setstate (char *__statebuf) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
344
  
345
  
346
  
347
  
348
  
349
  
350
  
351
struct random_data  
352
  {  
353
    int32_t *fptr;  
354
    int32_t *rptr;  
355
    int32_t *state;  
356
    int rand_type;  
357
    int rand_deg;  
358
    int rand_sep;  
359
    int32_t *end_ptr;  
360
  };  
361
  
362
extern int random_r (struct random_data *__restrict __buf,  
363
       int32_t *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
364
  
365
extern int srandom_r (unsigned int __seed, struct random_data *__buf)  
366
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));  
367
  
368
extern int initstate_r (unsigned int __seed, char *__restrict __statebuf,  
369
   size_t __statelen,  
370
   struct random_data *__restrict __buf)  
371
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 4)));  
372
  
373
extern int setstate_r (char *__restrict __statebuf,  
374
         struct random_data *__restrict __buf)  
375
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
376
  
377
  
378
  
379
  
380
  
381
  
382
extern int rand (void) __attribute__ ((__nothrow__ , __leaf__));  
383
  
384
extern void srand (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));  
385
  
386
  
387
  
388
  
389
extern int rand_r (unsigned int *__seed) __attribute__ ((__nothrow__ , __leaf__));  
390
  
391
  
392
  
393
  
394
  
395
  
396
  
397
extern double drand48 (void) __attribute__ ((__nothrow__ , __leaf__));  
398
extern double erand48 (unsigned short int __xsubi[3]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
399
  
400
  
401
extern long int lrand48 (void) __attribute__ ((__nothrow__ , __leaf__));  
402
extern long int nrand48 (unsigned short int __xsubi[3])  
403
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
404
  
405
  
406
extern long int mrand48 (void) __attribute__ ((__nothrow__ , __leaf__));  
407
extern long int jrand48 (unsigned short int __xsubi[3])  
408
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
409
  
410
  
411
extern void srand48 (long int __seedval) __attribute__ ((__nothrow__ , __leaf__));  
412
extern unsigned short int *seed48 (unsigned short int __seed16v[3])  
413
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
414
extern void lcong48 (unsigned short int __param[7]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
415
  
416
  
417
  
418
  
419
  
420
struct drand48_data  
421
  {  
422
    unsigned short int __x[3];  
423
    unsigned short int __old_x[3];  
424
    unsigned short int __c;  
425
    unsigned short int __init;  
426
    unsigned long long int __a;  
427
  };  
428
  
429
  
430
extern int drand48_r (struct drand48_data *__restrict __buffer,  
431
        double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
432
extern int erand48_r (unsigned short int __xsubi[3],  
433
        struct drand48_data *__restrict __buffer,  
434
        double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
435
  
436
  
437
extern int lrand48_r (struct drand48_data *__restrict __buffer,  
438
        long int *__restrict __result)  
439
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
440
extern int nrand48_r (unsigned short int __xsubi[3],  
441
        struct drand48_data *__restrict __buffer,  
442
        long int *__restrict __result)  
443
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
444
  
445
  
446
extern int mrand48_r (struct drand48_data *__restrict __buffer,  
447
        long int *__restrict __result)  
448
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
449
extern int jrand48_r (unsigned short int __xsubi[3],  
450
        struct drand48_data *__restrict __buffer,  
451
        long int *__restrict __result)  
452
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
453
  
454
  
455
extern int srand48_r (long int __seedval, struct drand48_data *__buffer)  
456
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));  
457
  
458
extern int seed48_r (unsigned short int __seed16v[3],  
459
       struct drand48_data *__buffer) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
460
  
461
extern int lcong48_r (unsigned short int __param[7],  
462
        struct drand48_data *__buffer)  
463
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
464
  
465
  
466
  
467
  
468
  
469
  
470
  
471
  
472
  
473
extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;  
474
  
475
extern void *calloc (size_t __nmemb, size_t __size)  
476
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;  
477
  
478
  
479
  
480
  
481
  
482
  
483
  
484
  
485
  
486
  
487
extern void *realloc (void *__ptr, size_t __size)  
488
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__warn_unused_result__));  
489
  
490
extern void free (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));  
491
  
492
  
493
  
494
  
495
extern void cfree (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));  
496
  
497
extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__));  
498
  
499
  
500
  
501
  
502
  
503
  
504
  
505
extern void *valloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;  
506
  
507
  
508
  
509
  
510
extern int posix_memalign (void **__memptr, size_t __alignment, size_t __size)  
511
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
512
  
513
  
514
  
515
  
516
extern void abort (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  
517
  
518
  
519
  
520
extern int atexit (void (*__func) (void)) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
521
  
522
extern int on_exit (void (*__func) (int __status, void *__arg), void *__arg)  
523
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
524
  
525
extern void exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  
526
  
527
  
528
extern void _Exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  
529
  
530
  
531
extern char *getenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
532
  
533
extern char *__secure_getenv (__const char *__name)  
534
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
535
extern int putenv (char *__string) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
536
extern int setenv (__const char *__name, __const char *__value, int __replace)  
537
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));  
538
extern int unsetenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
539
extern int clearenv (void) __attribute__ ((__nothrow__ , __leaf__));  
540
extern char *mktemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
541
extern int mkstemp (char *__template) __attribute__ ((__nonnull__ (1))) ;  
542
extern int mkstemps (char *__template, int __suffixlen) __attribute__ ((__nonnull__ (1))) ;  
543
extern char *mkdtemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
544
  
545
extern int system (__const char *__command) ;  
546
  
547
extern char *realpath (__const char *__restrict __name,  
548
         char *__restrict __resolved) __attribute__ ((__nothrow__ , __leaf__)) ;  
549
typedef int (*__compar_fn_t) (__const void *, __const void *);  
550
  
551
extern void *bsearch (__const void *__key, __const void *__base,  
552
        size_t __nmemb, size_t __size, __compar_fn_t __compar)  
553
     __attribute__ ((__nonnull__ (1, 2, 5))) ;  
554
extern void qsort (void *__base, size_t __nmemb, size_t __size,  
555
     __compar_fn_t __compar) __attribute__ ((__nonnull__ (1, 4)));  
556
extern int abs (int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;  
557
extern long int labs (long int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;  
558
  
559
__extension__ extern long long int llabs (long long int __x)  
560
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;  
561
  
562
extern div_t div (int __numer, int __denom)  
563
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;  
564
extern ldiv_t ldiv (long int __numer, long int __denom)  
565
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;  
566
  
567
  
568
__extension__ extern lldiv_t lldiv (long long int __numer,  
569
        long long int __denom)  
570
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;  
571
  
572
extern char *ecvt (double __value, int __ndigit, int *__restrict __decpt,  
573
     int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;  
574
extern char *fcvt (double __value, int __ndigit, int *__restrict __decpt,  
575
     int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;  
576
extern char *gcvt (double __value, int __ndigit, char *__buf)  
577
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;  
578
extern char *qecvt (long double __value, int __ndigit,  
579
      int *__restrict __decpt, int *__restrict __sign)  
580
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;  
581
extern char *qfcvt (long double __value, int __ndigit,  
582
      int *__restrict __decpt, int *__restrict __sign)  
583
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;  
584
extern char *qgcvt (long double __value, int __ndigit, char *__buf)  
585
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;  
586
extern int ecvt_r (double __value, int __ndigit, int *__restrict __decpt,  
587
     int *__restrict __sign, char *__restrict __buf,  
588
     size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));  
589
extern int fcvt_r (double __value, int __ndigit, int *__restrict __decpt,  
590
     int *__restrict __sign, char *__restrict __buf,  
591
     size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));  
592
extern int qecvt_r (long double __value, int __ndigit,  
593
      int *__restrict __decpt, int *__restrict __sign,  
594
      char *__restrict __buf, size_t __len)  
595
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));  
596
extern int qfcvt_r (long double __value, int __ndigit,  
597
      int *__restrict __decpt, int *__restrict __sign,  
598
      char *__restrict __buf, size_t __len)  
599
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));  
600
  
601
extern int mblen (__const char *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ;  
602
extern int mbtowc (wchar_t *__restrict __pwc,  
603
     __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ;  
604
extern int wctomb (char *__s, wchar_t __wchar) __attribute__ ((__nothrow__ , __leaf__)) ;  
605
extern size_t mbstowcs (wchar_t *__restrict __pwcs,  
606
   __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__));  
607
extern size_t wcstombs (char *__restrict __s,  
608
   __const wchar_t *__restrict __pwcs, size_t __n)  
609
     __attribute__ ((__nothrow__ , __leaf__));  
610
  
611
extern int rpmatch (__const char *__response) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
612
extern int getsubopt (char **__restrict __optionp,  
613
        char *__const *__restrict __tokens,  
614
        char **__restrict __valuep)  
615
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))) ;  
616
extern int getloadavg (double __loadavg[], int __nelem)  
617
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
618
  
619
extern int __VERIFIER_nondet_int(void);  
620
static void fail(void) {  
621
ERROR: __VERIFIER_error();  
622
}  
623
struct node {  
624
    struct node *next;  
625
    int value;  
626
};  
627
struct list {  
628
    struct node *slist;  
629
    struct list *next;  
630
};  
631
static void merge_single_node(struct node ***dst,  
632
                              struct node **data)  
633
{  
634
    struct node *node = *data;  
635
    *data = node->next;  
636
    node->next = ((void *)0);  
637
    **dst = node;  
638
    *dst = &node->next;  
639
}  
640
static void merge_pair(struct node **dst,  
641
                       struct node *sub1,  
642
                       struct node *sub2)  
643
{  
644
    while (sub1 || sub2) {  
645
        if (!sub2 || (sub1 && sub1->value < sub2->value))  
646
            merge_single_node(&dst, &sub1);  
647
        else  
648
            merge_single_node(&dst, &sub2);  
649
    }  
650
}  
651
static struct list* seq_sort_core(struct list *data)  
652
{  
653
    struct list *dst = ((void *)0);  
654
    while (data) {  
655
        struct list *next = data->next;  
656
        if (!next) {  
657
            data->next = dst;  
658
            dst = data;  
659
            break;  
660
        }  
661
        merge_pair(&data->slist, data->slist, next->slist);  
662
        data->next = dst;  
663
        dst = data;  
664
        data = next->next;  
665
        free(next);  
666
    }  
667
    return dst;  
668
}  
669
static void inspect_before(struct list *shape)  
670
{  
671
    do { if (!(shape)) fail(); } while (0);  
672
    for (; shape->next; shape = shape->next) {  
673
        do { if (!(shape)) fail(); } while (0);  
674
        do { if (!(shape->next)) fail(); } while (0);  
675
        do { if (!(shape->slist)) fail(); } while (0);  
676
        do { if (!(shape->slist->next == ((void *)0))) fail(); } while (0);  
677
    }  
678
    do { if (!(shape)) fail(); } while (0);  
679
    do { if (!(shape->next == ((void *)0))) fail(); } while (0);  
680
    do { if (!(shape->slist)) fail(); } while (0);  
681
    do { if (!(shape->slist->next == ((void *)0))) fail(); } while (0);  
682
}  
683
static void inspect_after(struct list *shape)  
684
{  
685
    do { if (!(shape)) fail(); } while (0);  
686
    do { if (!(shape->next == ((void *)0))) fail(); } while (0);  
687
    do { if (!(shape->slist != ((void *)0))) fail(); } while (0);  
688
    struct node *pos;  
689
    for (pos = shape->slist; pos->next; pos = pos->next);  
690
    do { if (!(!pos->next)) fail(); } while (0);  
691
}  
692
int main()  
693
{  
694
    struct list *data = ((void *)0);  
695
    while (__VERIFIER_nondet_int()) {  
696
        struct node *node = malloc(sizeof *node);  
697
        if (!node)  
698
            abort();  
699
        node->next = ((void *)0);  
700
        node->value = __VERIFIER_nondet_int();  
701
        struct list *item = malloc(sizeof *item);  
702
        if (!item)  
703
            abort();  
704
        item->slist = node;  
705
        item->next = data;  
706
        data = item;  
707
    }  
708
    if (!data)  
709
        return 0;  
710
    inspect_before(data);  
711
    while (data->next)  
712
        data = seq_sort_core(data);  
713
    inspect_after(data);  
714
    struct node *node = data->slist;  
715
    free(data);  
716
    while (node) {  
717
        struct node *snext = node->next;  
718
        free(node);  
719
        node = snext;  
720
    }  
721
    return 0;  
722
}  
DateTimeLevelComponentMessage
2025-08-2806:59:43:617INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2025-08-2806:59:43:697INFOCPAchecker.runCPAchecker 4.0 / terminationAnalysis (OpenJDK 64-Bit Server VM 17.0.15) started
2025-08-2806:59:43:715INFOCPAchecker.parseParsing CFA from file(s) "Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/merge_sort_true-unreach-call/merge_sort_true-unreach-call.c"
2025-08-2806:59:44:790INFOCFACreationUtils.addEdgeToCFAline 671: Dead code detected:
2025-08-2806:59:44:793INFOCFACreationUtils.addEdgeToCFAline 673: Dead code detected:
2025-08-2806:59:44:795INFOCFACreationUtils.addEdgeToCFAline 674: Dead code detected:
2025-08-2806:59:44:796INFOCFACreationUtils.addEdgeToCFAline 675: Dead code detected:
2025-08-2806:59:44:797INFOCFACreationUtils.addEdgeToCFAline 676: Dead code detected:
2025-08-2806:59:44:799INFOCFACreationUtils.addEdgeToCFAline 678: Dead code detected:
2025-08-2806:59:44:800INFOCFACreationUtils.addEdgeToCFAline 679: Dead code detected:
2025-08-2806:59:44:801INFOCFACreationUtils.addEdgeToCFAline 680: Dead code detected:
2025-08-2806:59:44:802INFOCFACreationUtils.addEdgeToCFAline 681: Dead code detected:
2025-08-2806:59:44:805INFOCFACreationUtils.addEdgeToCFAline 685: Dead code detected:
2025-08-2806:59:44:807INFOCFACreationUtils.addEdgeToCFAline 686: Dead code detected:
2025-08-2806:59:44:808INFOCFACreationUtils.addEdgeToCFAline 687: Dead code detected:
2025-08-2806:59:44:811INFOCFACreationUtils.addEdgeToCFAline 690: Dead code detected:
2025-08-2806:59:45:139INFOCoreComponentsFactory.createAlgorithmUsing Restarting Algorithm
2025-08-2806:59:45:161WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
cpa.arg.lateMerge
counterexample.export.exportWitness
2025-08-2806:59:45:162INFOCPAchecker.runAlgorithmStarting analysis ...
2025-08-2806:59:45:172INFORestartAlgorithm.runLoading analysis 1 from file /cpachecker/config/components/combinations-parallel-termination.properties ...
2025-08-2806:59:45:240INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
ResourceLimitChecker.fromConfiguration
Using the following resource limits: Thread CPU-time limit of 300s
2025-08-2806:59:45:635INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21.
2025-08-2806:59:46:037INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
PredicateCPA
PredicateCPARefiner.<init>
Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2025-08-2806:59:46:049WARNINGCPAs.retrieveCPAOrFailWarning: Skipping one analysis because the configuration file /cpachecker/config/components/combinations-parallel-termination.properties is invalid (TerminationAlgorithm needs a TerminationCPA)
2025-08-2806:59:46:052INFORestartAlgorithm.runLoading analysis 1 from file /cpachecker/config/components/termination-recursion.properties ...
2025-08-2806:59:46:062INFONestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/cpachecker/config/components/termination-recursion.properties': 'termination.config' has two values 'terminationAnalysis.properties' and 'termination-recursion.properties'. Using 'termination-recursion.properties'.
2025-08-2806:59:46:143WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
FormulaManagerView.<init>
Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics.
2025-08-2806:59:46:148INFOAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21.
2025-08-2806:59:46:382INFOAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
PredicateCPARefiner.<init>
Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2025-08-2806:59:46:453WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
FormulaManagerView.<init>
Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics.
2025-08-2806:59:46:487INFORestartAlgorithm.runStarting analysis 1 ...
2025-08-2806:59:46:488INFOAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.run0
Starting termination algorithm.
2025-08-2807:00:04:372WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
InequalityConverter.convert
Warning: Could not extract lasso (Loop with heads [N181]
incoming: [line 711: N180 -{while}-> N181]
outgoing: [line 711: N181 -{[(data->next) == 0]}-> N183]
nodes: [N181, N182, N184]
). (Unknown sort in equality)
2025-08-2807:00:04:381WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2807:01:40:860WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
InequalityConverter.convert
Warning: Could not extract lasso (Loop with heads [N142]
incoming: [line 689: N141 -{pos = shape->slist;}-> N142]
outgoing: [line 689: N142 -{[(pos->next) == 0]}-> N145]
nodes: [N142, N143, N144]
). (Unknown sort in equality)
2025-08-2807:01:40:863WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2807:01:41:419WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
InequalityConverter.convert
Warning: Could not extract lasso (Loop with heads [N188]
incoming: [line 716: N187 -{while}-> N188]
outgoing: [line 716: N188 -{[node__1 == 0]}-> N190]
nodes: [N188, N189, N191, N192, N193]
). (Unknown sort in equality)
2025-08-2807:01:41:420WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2807:01:54:913WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
InequalityConverter.convert
Warning: Could not extract lasso (Loop with heads [N31]
incoming: [line 654: N30 -{while}-> N31]
outgoing: [line 654: N31 -{[data == 0]}-> N33, line 656: N34 -{[next == 0]}-> N36]
nodes: [N31, N32, N34, N35, N40, N41, N42, N43, N44]
). (Unknown sort in equality)
2025-08-2807:01:54:914WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2807:02:08:202WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
InequalityConverter.convert
Warning: Could not extract lasso (Loop with heads [N31]
incoming: [line 654: N30 -{while}-> N31]
outgoing: [line 654: N31 -{[data == 0]}-> N33, line 656: N34 -{[next == 0]}-> N36]
nodes: [N31, N32, N34, N35, N40, N41, N42, N43, N44]
). (Unknown sort in equality)
2025-08-2807:02:08:203WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2807:02:21:452WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
InequalityConverter.convert
Warning: Could not extract lasso (Loop with heads [N31]
incoming: [line 654: N30 -{while}-> N31]
outgoing: [line 654: N31 -{[data == 0]}-> N33, line 656: N34 -{[next == 0]}-> N36]
nodes: [N31, N32, N34, N35, N40, N41, N42, N43, N44]
). (Unknown sort in equality)
2025-08-2807:02:21:453WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2807:02:21:655SEVERERefinementFailedException.forInterpolationFailureInSolverError: Refinement failed: Interpolation failed in solver MATHSAT5 with message 'can't build ie-local interpolant'.
Statistics NameStatistics ValueAdditional Value
Restart Algorithm statistics
Number of algorithms provided 2
Number of algorithms used 1
Last algorithm used /cpachecker/config/components/combinations-parallel-termination.properties
Total time for algorithm 1 156.483s
PredicateCPA statistics
Number of abstractions 829 3% of all post computations
Times abstraction was reused 0
Because of function entry/exit 0 0%
Because of loop head 800 97%
Because of join nodes 0 0%
Because of threshold 0 0%
Because of target state 29 3%
Times precision was empty 195 24%
Times precision was {false} 18 2%
Times result was cached 280 34%
Times cartesian abs was used 0 0%
Times boolean abs was used 336 41%
Times result was 'false' 123 15%
Number of strengthen sat checks 0
Number of coverage checks 5947
BDD entailment checks 628
Number of SMT sat checks 0
trivial 0
cached 0
Max ABE block size 19
Avg ABE block size 7.72 sum: 6402, count: 829, min: 0, max: 19
Number of predicates discovered 23
Number of abstraction locations 5
Max number of predicates per location 7
Avg number of predicates per location 4
Total predicates per abstraction 2280
Max number of predicates per abstraction 8
Avg number of predicates per abstraction 6.44
Number of irrelevant predicates 594 26%
Number of preds handled by boolean abs 1066 47%
Total number of models for allsat 1225
Max number of models for allsat 28
Avg number of models for allsat 3.65
Time for post operator 1.575s
Time for path formula creation 1.553s
Time for strengthen operator 0.043s
Time for prec operator 1.194s
Time for abstraction 1.111s Max: 0.022s, Count: 829
Boolean abstraction 0.557s
Solving time 0.266s Max: 0.012s
Model enumeration time 0.253s
Time for BDD construction 0.065s Max: 0.001s
Time for merge operator 0.093s
Time for coverage checks 0.019s
Time for BDD entailment checks 0.012s
Total time for SMT solver (w/o itp) 0.519s
Number of path formula cache hits 18550 69%
Inside post operator
Inside path formula creation
Time for path formula computation 1.477s
Total number of created targets for pointer analysis 0
Number of BDD nodes 1226
Size of BDD node table 466043
Size of BDD cache 46619
Size of BDD node cleanup queue 0.38 sum: 1307, count: 3424, min: 0, max: 547
Time for BDD node cleanup 0.004s
Time for BDD garbage collection 0.000s in 0 runs
KeyValue statistics
Init. function predicates 0
Init. global predicates 0
Init. location predicates 0
Invariant Generation statistics
AutomatonAnalysis (NonTerminationLabelAutomaton) statistics
Number of states 1
Total time for successor computation 0.108s
Automaton transfers with branching 0
Automaton transfer successors 0.97 sum: 23125, count: 23753, min: 0, max: 1 [0 x 628, 1 x 23125]
Number of states with assumption transitions 0
AutomatonAnalysis (TerminatingFunctions) statistics
Number of states 1
Total time for successor computation 0.029s
Automaton transfers with branching 0
Automaton transfer successors 0.99 sum: 23001, count: 23125, min: 0, max: 1 [0 x 124, 1 x 23001]
Number of states with assumption transitions 0
Termination Algorithm statistics
Total time 155.165s
Time for recursion analysis 0.000s
Number of analysed loops 4 57%
Total time for loop analysis 155.160s
Avg time per loop analysis 38.790s
Max time per loop analysis 96.290s
Number of safety analysis runs 10
Avg safety analysis run per loop 2.50
Max safety analysis run per loop 4 for loops [N31]
Total time for safety analysis 5.564s
Avg time per safety analysis run 0.556s
Max time per safety analysis run 2.942s
Number of analysed lassos 0
Avg number of lassos per loop 0.00
Max number of lassos per loop 0 for loops
Avg number of lassos per iteration 0.00
Max number of lassos per iteration 0
Total time for lassos analysis 149.558s
Avg time per iteration 24.926s
Max time per iteration 95.029s
Time for lassos construction 149.558s
Avg time for lasso construction per iteration 24.926s
Max time for lasso construction per iteration 95.029s
Time for stem and loop construction 0.210s
Avg time for stem and loop construction per iteration 0.035s
Max time for stem and loop construction per iteration 0.111s
Time for lassos creation 149.319s
Avg time for lassos creation per iteration 24.886s
Max time for lassos creation per iteration 94.978s
Total time for non-termination analysis 0.000s
Avg time for non-termination analysis per lasso 0.000s
Max time for non-termination analysis per lasso 0.000s
Total time for termination analysis 0.000s
Avg time for termination analysis per lasso 0.000s
Max time for termination analysis per lasso 0.000s
Total number of termination arguments 0
Avg termination arguments per loop 0.00
Max termination arguments per loop 0 for loops
Counterexample-Check Algorithm statistics
Number of counterexample checks 0
Termination Algorithm statistics
Total time 155.165s
Time for recursion analysis 0.000s
Number of analysed loops 4 57%
Total time for loop analysis 155.160s
Avg time per loop analysis 38.790s
Max time per loop analysis 96.290s
Number of safety analysis runs 10
Avg safety analysis run per loop 2.50
Max safety analysis run per loop 4 for loops [N31]
Total time for safety analysis 5.564s
Avg time per safety analysis run 0.556s
Max time per safety analysis run 2.942s
Number of analysed lassos 0
Avg number of lassos per loop 0.00
Max number of lassos per loop 0 for loops
Avg number of lassos per iteration 0.00
Max number of lassos per iteration 0
Total time for lassos analysis 149.558s
Avg time per iteration 24.926s
Max time per iteration 95.029s
Time for lassos construction 149.558s
Avg time for lasso construction per iteration 24.926s
Max time for lasso construction per iteration 95.029s
Time for stem and loop construction 0.210s
Avg time for stem and loop construction per iteration 0.035s
Max time for stem and loop construction per iteration 0.111s
Time for lassos creation 149.319s
Avg time for lassos creation per iteration 24.886s
Max time for lassos creation per iteration 94.978s
Total time for non-termination analysis 0.000s
Avg time for non-termination analysis per lasso 0.000s
Max time for non-termination analysis per lasso 0.000s
Total time for termination analysis 0.000s
Avg time for termination analysis per lasso 0.000s
Max time for termination analysis per lasso 0.000s
Total number of termination arguments 0
Avg termination arguments per loop 0.00
Max termination arguments per loop 0 for loops
Counterexample-Check Algorithm statistics
Number of counterexample checks 0
Code Coverage
Function coverage 0.857
Visited lines 321
Total lines 336
Line coverage 0.955
Visited conditions 44
Total conditions 56
Condition coverage 0.786
CPAchecker general statistics
Number of program locations 440
Number of CFA edges (per node) 448 count: 440, min: 0, max: 2, avg: 1.02
Number of relevant variables 19
Number of functions 7
Number of loops (and loop nodes) 7 sum: 76, min: 3, max: 27, avg: 10.86
Size of reached set 573
Number of reached locations 89 20%
Avg states per location 6
Max states per location 35 at node N1
Number of reached functions 6 86%
Number of partitions 89
Avg size of partitions 6
Max size of partitions 35 with key N1
Number of target states 1
Size of final wait list 11
Time for analysis setup 1.447s
Time for loading CPAs 0.020s
Time for loading parser 0.210s
Time for CFA construction 1.171s
Time for parsing file(s) 0.414s
Time for AST to CFA 0.366s
Time for CFA sanity check 0.061s
Time for post-processing 0.197s
Time for loop structure 0.012s
Time for AST structure 0.000s
Time for CFA export 0.681s
Time for function pointers resolving 0.004s
Function calls via function pointers 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables 0.095s
Time for collecting variables 0.056s
Time for solving dependencies 0.004s
Time for building hierarchy 0.000s
Time for building classification 0.029s
Time for exporting data 0.006s
Time for Analysis 156.484s
CPU time for analysis 189.300s
Total time for CPAchecker 157.943s
Total CPU time for CPAchecker 191.820s
Time for statistics 0.189s
Time for Garbage Collector 2.013s in 1934 runs
Garbage Collector(s) used PS MarkSweep, PS Scavenge
Used heap memory 206MB ( 196 MiB) max; 108MB ( 103 MiB) avg; 219MB ( 209 MiB) peak
Used non-heap memory 68MB ( 65 MiB) max; 65MB ( 62 MiB) avg; 70MB ( 66 MiB) peak
Used in PS Old Gen pool 122MB ( 116 MiB) max; 69MB ( 66 MiB) avg; 122MB ( 116 MiB) peak
Allocated heap memory 263MB ( 251 MiB) max; 260MB ( 248 MiB) avg
Allocated non-heap memory 71MB ( 68 MiB) max; 69MB ( 66 MiB) avg
Total process virtual memory 14982MB ( 14288 MiB) max; 14964MB ( 14271 MiB) avg
#Configuration NameConfiguration Value
1analysis.algorithm.termination true
2analysis.machineModel Linux64
3analysis.name terminationAnalysis
4analysis.programNames Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/merge_sort_true-unreach-call/merge_sort_true-unreach-call.c
5analysis.restartAfterUnknown true
6counterexample.export.exportWitness false
7cpa.arg.lateMerge prevent
8language C
9log.level INFO
10parser.usePreprocessor true
11restartAlgorithm.configFiles components/combinations-parallel-termination.properties, components/termination-recursion.properties::if-recursive
12specification
13statistics.print true
14termination.config terminationAnalysis.properties

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

{{dependency.name}} {{dependency.version}}

Source: {{dependency.repository}}

{{dependency.copyright}}

License:

Full text of license
{{dependencies.licenses[dependency.licenseId]}}